Linearized model leads to UNSAT or unfeasible solutions given the bound

[raphaelboudreault]

OS: Linux Ubuntu 22.04
MZN version: 2.9.2

Hello! I am currently working on a MiniZinc model involving float and integer variables, using a linear solver (in my case, SCIP 8.0.4). In the model, I have an array of float variable declared under the form array[X, Y] of var 0.0..<float bound>: x, involved in numerous constraints. However, depending on the value used for <float bound>, I am getting different results. Using a value of 1000.0, the returned solution is optimal and as expected. Using instead a value of 100000000.0, the solver returns UNSAT. See attached the generated FZN in both cases, which differ only by a factor in the domains and paremeters. Clearly, this is not an expected behavior, and I wonder if it is related to MiniZinc or the solver. CPLEX allows instead an unfeasible solution using the biggest value.

On another note, using

array[X, Y] of var float: x
constraint forall(i in X, j in Y)(x[i, j] >= 0 /\ x[i, j] <= <float bound>)

leads to

MiniZinc: flattening error: unbounded coefficient in linear expression. Make sure variables involved in non-linear/logical expressions have finite bounds in their definition or via constraints

where I felt like the two formulations should be equivalent from the point of view of MiniZinc.
Thanks!

linear_NO.txt
linear_OK.txt

[ImadAziez]

Hello, I am facing a similar issue when working with float and integer variables in MiniZinc. I’ve noticed that when I change the upper bound for my float variables, I also get different results from the solver. I haven’t found a solution yet, and I’m wondering if anyone has come across this issue or if there's a workaround. Thank you!

[raphaelboudreault]

Has this has been reproduced by the MiniZinc team and identified as a bug? @Dekker1

[Dekker1]

It certainly sounds like a bug, and I get the same results when running the two FlatZinc files, but without a smaller example, that is preferably written in MiniZinc, it will be very challenging to diagnose where the problem lies.

[raphaelboudreault]

Thanks for the reply. We will try to build a small example and provide you with the MZN file.

[ImadAziez]

Hello @Dekker1. Please find attached the files for a minimum working example.

The bug can be reproduced by alternating the value of the parameter typeD_upper_bound in the JSON file and using CPLEX as a solver. Specifically:

When typeD_upper_bound = 100000, the solver produces the following results:

n_a_d = 2.115330576896667

n_m_d = 2.115330576896667

l_us = 5.270305432771382e-05

When typeD_upper_bound = 1000000000, the results change to:

n_a_d = 0.001001031509929362

n_m_d = 0.001001031509929362

l_us = 5.270422266158761e-05

export_mzn.json

mip_model.txt

A potential debugging tip: I noticed that in Constraint 10, replacing = with <= produces the same solver output for both values of the parameter typeD_upper_bound. However, I'm not entirely sure if this is the root cause of MiniZinc's behavior. Let me know if you need any additional details.

Thank you!